$\forall$${\it es}$:ES, ${\it Qa}$, ${\it Rb}$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$), $f$, $g$:Top.
\\[0ex]es{-}interface{-}empty(${\it es}$;${\it Ia}$) $\Rightarrow$ es{-}interface{-}empty(${\it es}$;${\it Ib}$) $\Rightarrow$ $g$ glues ${\it Ia}$:${\it Qa}$ $--$$f$$\rightarrow$ ${\it Ib}$:${\it Rb}$